| Definitions | id-deq, ecl-kinds(x), EqDecider(T), lnk(k), fpf-dom(eq; x; f), Kind-deq, fpf-all(A; eq; f; x,v.P(x;v)), normal-da{i:l}(da), ecl(ds; da), normal-ds{i:l}(ds), rec(x.A(x)), decl-state(ds), fpf(A; a.B(a)), atom{$n:n}, ecl-machine1{$ecl:ut2}(i; ds; da; A), destination(l), isrcv(k), normal-type{i:l}(T), [], cons(car; cdr), subtype(S; T), isect(A; x.B(x)), void, ||as||, ge(i; j), left + right, sqequal(s; t), sq_type(T), guard(T), R-realizes{i:l}(R; es.P(es)), R-Feasible{i:l}(R), R-consistent(R; es), l_all(L; T; x.P(x)), es-first(es; e), es-kind(es; e), R-state-var-init(i; ds; da; x; T; v; ks; tr), fpf-compatible(A; a.B(a); eq; f; g),  x.A(x), es-bact{i:l}(ds; da; a; es; n; e1; e2), fpf-cap(f; eq; x; z), top, Type, ma-valtype(da; k), es-valtype(es; e), loc(e), es-init(es;e),  , event_system{i:l}, <a, b>,  , A  B,  A, False, (x  l), Knd, es-dtype(es; i; x; T), es-decls(es;i;ds;da), A c B, alle-at(es; i; e.P(e)),  x. t(x), {x:A| B(x)} , Id, es-E(es), P Q, x:A  B(x), P   Q, prop{i:l}, es-after(es; x; e), es-trans-state-from{i:l}(es;ks;g;z;e1;e2), x:A  B(x), es-when(es; x; e), t T, es-vartype(es; i; x), ecl-trans-type(A), ecl-trans-ks(v), ecl-trans-a(v), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)),  b, mkid{$x:ut2}, ecl-trans(x), ecl-trans-tuple{i:l}(ds; da), s = t, ecl-trans-act(ds; da; A), f(a), ecl-act(ds; da; m; x), P  Q,  ,  x:A. B(x), event-info(ds;da), type List, let x = a in b(x), fpf-ap(f; eq; x), fpf-domain(f), es-isconst(es; i; x), case b of inl(x) => s(x) | inr(y) => t(y), True, ff, tt, if b then t else f fi , kind(e), x,y. t(x;y), loc(e), first(e), SWellFounded(R(x;y)), pred!(e;e'), es-le(es; e; e'), eq_id(a; b), P  Q, es-isrcv(es; e), let x,y = A in B(x;y), constant_function(f; A; B), qle(r; s), e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), rationals, Msg(M), kindcase(k; a.f(a); l,t.g(l;t)), EState(T), EOrderAxioms(E;pred?;info), Unit, suptype(S; T), l[i], #$n, IdLnk, a < b, t.1, l-all(L; x.P(x)), P Q, es-state-when(es; e), es-state(es; i), es-val(es; e), es-rcvtype(es; e), es-acttype(es; e), locl(a), rcv(l,tg), es-hist{i:l}(es;e1;e2),  x:A. B(x), append(as; bs), spreadn(a; x,y,z.t(x;y;z)), decidable(P), ecl-trans-state(v; L), ecl-trans-init(v), ecl-trans-state-from(v; z; L), es-info(es;e), ecl-es-act(es; m; x),  , @i discrete ds, t ...$L, n + m, es-causl(es; e; e'), es-locl(es; e; e'), [e, e'], es-pred(es; e) |
| Lemmas | es-hist-last, es-interval-eq2, es-after-pred2, es-after-pred, ecl-trans-state wf, es-loc-pred, general-append-cancellation, es-pred wf, es-interval wf, map append sq, es-first-init, es-init-le, l member subtype, es-interval-less-sq, length append, length cons, length nil, es-info wf, es-interval-eq, es-init-elim2, es-init-elim, decidable assert, assert-es-bact, es-hist wf, append wf, iff functionality wrt iff, ecl-es-act-ecl-act, es-valtype wf, rcv wf, locl wf, es-acttype wf, es-rcvtype wf, es-val wf, subtype rel self, subtype rel dep function, es-state-subtype, es-state-subtype2, es-state-when wf, nat properties, rev implies wf, le wf, fpf-cap wf, IdLnk wf, select wf, length wf1, ext-eq weakening, subtype rel weakening, es-isrcv wf, assert-eq-id, es-loc-init, es-le-loc, Id sq, es-isrcv-loc, es-trans-state-from wf, es-decls-iff, unit wf, first wf, constant function wf, EState wf, kindcase wf, rationals wf, qle wf, cless wf, val-axiom wf, Msg wf, loc wf, kind wf, EOrderAxioms wf, deq wf, btrue wf, bfalse wf, false wf, true wf, es-isconst wf, es-when wf, es-after wf, alle-at wf, es-init wf, assert wf, es-bact wf, iff wf, fpf-compatible-single, R-state-var-init wf, nat wf, es-loc wf, es-E wf, es-kind wf, l member wf, es-vartype wf, es-first wf, es-dtype wf, es-decls wf, R-implies-rule, event system wf, R-consistent wf, Knd sq, cons one one, non neg length, top wf, length wf nat, isrcv wf, R-state-var-init-rule, ecl-trans-ks wf, ecl-trans-act wf, ecl-act wf, ecl-trans-tuple wf, ecl-trans wf, ecl-kinds-ecl-trans, ecl-trans-property, event-info wf, Id wf, Knd wf, bool wf, ma-valtype wf, decl-state wf, normal-ds wf, normal-da wf, fpf-trivial-subtype-top, Kind-deq wf, fpf-dom wf, lnk wf, ldst wf, ecl-kinds wf, l all wf2, id-deq wf, not wf |
